begin_problem(Pelletier54).

list_of_descriptions.
name({*Pelletier's Problem No. 54*}).
author({*Christoph Weidenbach*}).
status(unsatisfiable).
description({*Problem taken in revised form from the "Pelletier Collection", Journal of Automated
	Reasoning, Vol. 2, No. 2, pages 191-216*}).
end_of_list.

list_of_symbols.
 functions[(time,1), (ai,0), (math,0), (databases,0), (alice,0)].
 predicates[(student,1),(professor, 1), (course, 1), (enrolled, 2), (teaches, 2), (prereq, 2), (completed, 2)].
end_of_list.


list_of_formulae(axioms).

% Rule 1
formula(forall([C],
   implies(
     course(C),
     exists([P], teaches(P,C))
    )
)).

% Rule 2
formula(forall([S,C],
  implies(
     enrolled(S,C),
     course(C)
   )
)).

% Rule 3
formula(forall([S,C],
  implies(
    enrolled(S,C),
    forall([P],  implies(prereq(P,C), completed(S,P)))
  )
)).

% Rule 4
formula(forall([S,C1,C2],
  implies(
     and(enrolled(S,C1), enrolled(S,C2), equal (time(C1),time(C2))),
      equal(C1,C2)
   )
)).

% Rule 5
formula(forall([P],
  implies(
     professor(P),
     exists([C], teaches(P,C))
   )
)).

% Rule 6
formula(forall([C],
     not(prereq(C,C))
)).


formula(student(alice)).

formula(course(ai)).
formula(course(math)).
formula(course(databases)).

% Logic is prerequisite for AI
formula(prereq(math,ai)).

% Alice enrolled in AI
formula(enrolled(alice,ai)).

% Alice enrolled in Databases
formula(enrolled(alice,databases)).

% AI and Databases overlap
formula(equal(time(databases), time(ai))).

% Alice did not complete Logic
formula(not(completed(alice,math))).

% Distinct courses
formula(not(equal(ai,databases))).



end_of_list.




list_of_formulae(conjectures).


end_of_list.
% this is a comment. We like comments ;-)
list_of_settings(SPASS).
{*
set_flag(PGiven,1).
set_flag(PProblem,0).
*}
end_of_list.

end_problem.
  